Nuprl Lemma : Namer-subtype
11,40
postcript
pdf
n
,
m
:
,
L
,
L'
:(Id List). (
n
m
)
L
L'
(Namer(
m
;
L'
)
r Namer(
n
;
L
))
latex
Definitions
{
x
:
A
|
B
(
x
)}
,
,
type
List
,
A
,
A
B
,
(
x
l
)
,
x
L
.
P
(
x
)
,
x
:
A
B
(
x
)
,
s
=
t
,
Inj(
A
;
B
;
f
)
,
{
i
..
j
}
,
False
,
t
T
,
Id
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
A
c
B
,
P
&
Q
,
x
:
A
B
(
x
)
,
Void
,
i
j
<
k
,
S
T
,
a
<
b
,
suptype(
S
;
T
)
,
<
a
,
b
>
,
Type
,
x
.
t
(
x
)
,
Namer(
n
;
Id_list
)
,
A
B
,
f
(
a
)
,
,
#$n
Lemmas
le
wf
,
l
member
wf
,
subtype
rel
set
,
nat
properties
origin
n, m:
, L, L':(Id List). (n 
m) 
L 
L' (Namer(m;L') r Namer(n;L)) n, m:, L, L':(Id List). (n m) L L' (Namer(m;L') r Namer(n;L)) 
A B
l)xL. P(x)
B(x)
} T Qx:A. B(x)
B
B(x) j < k T
x. t(x) B